ePMC

Benchmark
Model:csma v.1 (MDP)
Parameter(s)N = 3, K = 4
Property:all_before_max (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files csma.3-4.prism --model-input-type prism --property-input-files csma.props --property-input-names all_before_max --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6
Execution
Walltime:83.99754905700684s
Return code:0
Relative Error:4.780713336828581e-07
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property all_before_max
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 12803 12803
build-model-states-explored 30199 17396
build-model-states-explored 47078 16879
build-model-states-explored 64456 17378
build-model-states-explored 80425 15969
build-model-states-explored 98413 17988
build-model-states-explored 115245 16832
build-model-states-explored 130357 15112
build-model-states-explored 149351 18994
build-model-states-explored 169419 20068
build-model-states-explored 188444 19024
build-model-states-explored 208251 19808
build-model-states-explored 227463 19212
build-model-states-explored 247557 20094
build-model-states-explored 263120 15563
build-model-states-explored 282139 19019
build-model-states-explored 302212 20072
build-model-states-explored 321656 19445
build-model-states-explored 342019 20362
build-model-states-explored 361347 19329
build-model-states-explored 381675 20328
build-model-states-explored 402240 20565
build-model-states-explored 422291 20051
build-model-states-explored 442241 19950
build-model-states-explored 461367 19126
build-model-states-explored 482088 20721
build-model-states-explored 502785 20697
build-model-states-explored 518480 15695
build-model-states-explored 534267 15787
build-model-states-explored 554553 20286
build-model-states-explored 573409 18856
build-model-states-explored 593642 20232
build-model-states-explored 614072 20431
build-model-states-explored 634474 20402
build-model-states-explored 654920 20446
build-model-states-explored 674808 19888
build-model-states-explored 694828 20020
build-model-states-explored 714970 20142
build-model-states-explored 735357 20387
build-model-states-explored 755336 19979
build-model-states-explored 774747 19411
build-model-states-explored 794366 19619
build-model-states-explored 814293 19927
build-model-states-explored 834221 19928
build-model-states-explored 853687 19466
build-model-states-explored 873266 19578
build-model-states-explored 893252 19987
build-model-states-explored 913140 19888
build-model-states-explored 932606 19466
build-model-states-explored 952387 19781
build-model-states-explored 972324 19937
build-model-states-explored 991865 19541
build-model-states-explored 1011436 19571
build-model-states-explored 1031368 19932
build-model-states-explored 1041019 9651
build-model-states-explored 1054301 13282
build-model-states-explored 1074199 19898
build-model-states-explored 1094340 20141
build-model-states-explored 1114370 20030
build-model-states-explored 1134569 20199
build-model-states-explored 1154476 19907
build-model-states-explored 1174514 20038
build-model-states-explored 1194703 20189
build-model-states-explored 1214493 19790
build-model-states-explored 1234822 20329
build-model-states-explored 1254620 19797
build-model-states-explored 1272561 17942
build-model-states-explored 1292452 19891
build-model-states-explored 1312534 20082
build-model-states-explored 1332581 20047
build-model-states-explored 1352668 20087
build-model-states-explored 1372830 20161
build-model-states-explored 1393024 20194
build-model-states-explored 1413079 20056
build-model-states-explored 1433413 20334
build-model-states-explored 1454005 20592
build-model-done 1460287 76
iterating
iterating-progress-unbounded 107 88.0 1
iterating-done 173 1
model-checking-done 83
command-check-result-is 0.9324464830696655 all_before_max